A:Type, B, C, D:(AType), f:a:A fp B(a), g:a:A fp C(a), eq:EqDecider(A).
(a:A. (a  dom(f))  (B(a) r D(a)))
 (a:A. (a  dom(g))  (C(a) r D(a)))
 (f  g  a:A fp D(a)) 

latex

Definitions	x:A. B(x), a:A fp B(a), x(s), P  Q, x  dom(f), t  T, x. t(x), S  T, suptype(S; T), t.1, T, True, , SqStable(P), P  Q, P  Q, P & Q
Lemmas	fpf-join wf, l member wf, sq stable from decidable, assert wf, deq-member wf, decidable assert, assert-deq-member, fpf-dom wf, fpf-trivial-subtype-top, deq wf, fpf wf